Nuprl Lemma : decidable__l_member
0,22
postcript
pdf
A
:Type,
x
:
A
. (
x
,
y
:
A
. Dec(
x
=
y
))
(
L
:
A
List. Dec((
x
L
)))
latex
Definitions
Dec(
P
)
,
False
,
x
:
A
.
B
(
x
)
,
Prop
,
t
T
,
(
x
l
)
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
decidable
wf
,
cons
member
,
decidable
or
,
decidable
functionality
,
nil
member
,
l
member
wf
,
false
wf
,
decidable
false
origin